『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 3 Sets and logic
『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 2 Homotopy type theory ←
→ 『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 4 Equivalences
P107-P128
型と論理
Definition 3.1.1. A type A is a set if for all x, y : A and all p, q : x = y, we have p = q. More precisely, the proposition isSet(A) is defined to be the type
$ \mathrm{isSet}(A) :\equiv \prod_{(x,y:A)}\prod_{(p,q:x=y)} (p = q)
#型と集合 #型と論理
#文献